The design and testing of software is often an expensive and time-consuming process. Tools based on model checking with automaton specifications have been very effective at finding important bugs such as buffer overflows, memory safety violations, and violations of locking and security policies. In general, a sound program analysis tool will not miss any errors. If the tool reports no potential problems, then the analyzed program is said to be error-free (for the class of errors that the tool checks). The correctness problem, however, is undecidable (i.e., the problem cannot be solved precisely). Thus, problems reported by sound tools may contain false alarms. The challenge in developing a precise tool is to keep the false alarm ratio low.
Static program analysis tools may reduce the false alarm ratio by performing a two-phase analysis. In a first phase, a quick, approximate analysis of the program may be performed to detect potential errors. A state exploration algorithm, such as depth-first search (DFS), is typically employed to visit all reachable states in a control flow graph. Each visited state can be evaluated to determine if the state satisfies one or more predefined correctness properties. Typically, when an error state is encountered, a stack data structure maintained by the DFS algorithm will contain a path from the entry state to the error state.
In a second phase, the precision can be improved by subjecting the stack path to a feasibility check. Each potential error trace may be examined in detail, applying theorem proving techniques to check whether the trace is feasible, i.e., whether it is possible for a real program execution to follow the trace all the way to the error. If the feasibility test determines that the trace is feasible, the problem is reported, and if it determines that the trace is infeasible, the report is suppressed. For a discussion of such feasibility checks, see, for example, D. Dams and K. Namjoshi, “Orion: High Precision Methods for Static Error Analysis of C and C++ Programs,” downloadable from http://cm.bell-labs.com/who/dennis/Papers/dn04c.pdf or D. Brand, “A Software Falsifier,” Int'l Symp. on Software Reliability Engineering, 174-185 (October, 2000), each incorporated by reference herein.
While such feasibility checks may increase the precision of the error checking, one or more errors may get masked. In particular, if a path to an error state is infeasible (and hence not reported), then another subsequently processed feasible path to the same state may be missed by the search. Generally, a DFS algorithm will backtrack when it encounters a state that has been visited before. Thus, by adding a feasibility check, DFS may become an unsound method for detecting reachable errors. It has been found that DFS is an algorithm for exploring states of a graph, not paths through the graph.
State Space Caching, a generalization of the DFS algorithm, is another well-known technique for exploring reachable states of a graph in which only a subset of the visited states is kept in memory (cached). A State Space Caching algorithm may enumerate the (non-looping) paths in a graph, by using a cache of size zero. J. Geldenhuys, “State Caching Reconsidered,” SPIN, 23-38 (2004) provides an overview of various criteria that have been proposed for the selection of states to be kept in the cache. For example, when the goal of the algorithm is to explore states, random replacement of cached states is a reasonable strategy.
A need exists for improved methods and apparatus for exploring paths through a graph representation of a program or another entity.